package agent.ccs
import cwb.Module
import cwb.Command
import scala.util.parsing.combinator.RegexParsers
import cwb.CWBCommands
import cwb.Polygraph

/**
 * HelperParser is a unified parser for handing reading of and assignment to agents or relabellings
 * depending upon whether isAgParser is true or false.
 */
class HelperParser(isAgParser: Boolean) extends CCSParser {
  val command = if (isAgParser) AgentCommand else RelabelCommand
      private val incorrectString = """[a-z][a-zA-Z0-9']*""".r
      // Agents/ Relabellings have to start with an uppercase letter
      private val correctString = """[A-Z][a-zA-Z0-9']*""".r

      private def incorrectVar: Parser[Unit] = incorrectString ^^ {
      case _ => println("*** Expected a variable but found a (ie. an Actt) ***")
  }

  def correctVar: Parser[String] = correctString

      def assignment: Parser[Unit] = correctVar ~ "=" ~ (if (isAgParser) agent else litRelabel) ^^ {
      case str ~ "=" ~ (ag: PrivateAgent) => {
        val sym = Symbol(str)
            // Remove any possible current definition.
        val agent = CCSAgent.makeAgent(ag)
            CCSComponent.environment.clearBinding(sym)
            // TODO Clean up: Pessimisticly clearing the polygraph table.
            Polygraph.table.clear()
            CCSComponent.environment.insertBinding(str, agent)  
      }

      case str ~ "=" ~ (relabel: LitRelabel) => {
        // Remove any possible current definition.
        val sym = Symbol(str)
            CCSComponent.environment.clearRelabel(sym)
            CCSComponent.environment.putRelabel(sym, relabel)  
      }

      }

      def definition: Parser[Unit] = correctVar ^^ {
      case str => {
        val sym = Symbol(str)
            if (isAgParser) {
              CCSComponent.environment.getAgent(sym) match {
              case Some(x) => CCSComponent.printAgent(sym, x)
              case _ => println(sym + " is unbound")
              }
            } else {
              CCSComponent.environment.getRelabel(sym) match {
              case x => CCSComponent.printRelabel(sym, x)
              }
            }
      }
      }

      def acceptable = assignment | definition


        def run(input: String) {
        parseAll(acceptable, input) match {
        case failure: NoSuccess => {
          println(failure.msg)

          println("Parse failed. Usage: \n " + command.helpDetailed)
        }
        case _ =>
        }
      }
}

abstract trait CCSCommand extends Command {
  protected def run(input: String)
  
  def apply(input: String) = {
    // Ensure counts for variable lookups are cleared before running a new command.
    CCSComponent.environment.clearAccesses()
    run(input)
  }
}

object AgentCommand extends CCSCommand {
  val name = "agent"
      val helpShort = "change (or show) the definition of an agent identifier"
      val helpDetailed = "agent X = A;" + 
          "\nbinds agent A to identifier X" +
          "\nagent X(FP) = A;" +
          "\nagent X;" +
          "\nprints the definition of X" +
          "\n\nAn agent identifier must begin with an upper case letter."

  private val parser = new HelperParser(true)
  def run(input: String) = parser.run(input)
}


/**
 * RelabelCommand is a top level CWB command which binds a relabel definition to an identifier. 
 */
object RelabelCommand extends CCSCommand {
  val name = "relabel"
      val helpShort =  "change (or show) the definition of a relabelling identifier"
      val helpDetailed = "  relabel R = [a/p,...];" +
          "\nbinds a relabelling function" +
          "\nrelabel R;" +
          "\nprints function bound to R" +
          "\n" +
          "\na/p means that p is relabelled to a. You cannot relabel tau." +
          "\nIf p is relabelled to a, then 'p is also relabelled to 'a. You cannot" +
          "\ndefine a relabelling function which violates this rule."

  private val parser = new HelperParser(false)  

  def run(input: String) = parser.run(input)
}

/**
 * ClearCommand is a top level CWB command which clears all bindings of the global environment.
 */
object ClearCommand extends CCSCommand {
  val name = "clear"
      val helpShort =  "removes all bindings (a fresh start)"
      val helpDetailed = "Clears bindings to all agents and relabellings"

  def run(input: String) = CCSComponent.clearEnv()
}


/**
 * PrintCommand is a top level CWB command used to print all defined agents and relabelings.
 */
object PrintCommand extends CCSCommand {
  val name = "print"
      val helpShort = "show the definitions of all identifiers"
      val helpDetailed = "print;" + 
          "\n" +
          "\nTo print just one binding, say that of agent A, use `agent A;'. Etc." +
          "\n" +
          "See also: agent, set, relabel, prop, save" 

  def run(input: String) = {
    // Sorts a list of (symbol, agent) by the string associated to the symbol.
    
    val sorted_agents = CCSComponent.environment.agentsAsList.sortWith {
      case ((s1, _),(s2, _)) => s1.name < s2.name
    }
    
    if (sorted_agents.size != 0) println("** Agents **")

    sorted_agents foreach {
    case (sym, ag) => CCSComponent.printAgent(sym, ag)
    }
    println()
    
    val sorted_relabellings = CCSComponent.environment.relabelsAsList.sortWith {
      case ((s1, _),(s2, _)) => s1.name < s2.name
    }
    
    
    if (sorted_relabellings.size != 0) println("** Relabelling functions **")
    sorted_relabellings foreach {
      case (sym, rel) => CCSComponent.printRelabel(sym, rel)
    }
    
    // (sym, ag) => println(sym.name)
    if (input.replace(" ", "") != "") {
      println("*** Extra input found, to print a single agent, use agent <identifier>")
    }
  }
}


/**
 * Top level CWB command used to output transitions of the given agent input string.
 */
object TransitionsCommand extends CCSCommand {
  val name = "transitions"
      val helpShort = "list the (single-step) transitions of an agent"
      val helpDetailed = "transitions A;"
      def run(input: String) = {
    val agent = CCSComponent.parser.readAgent(input)
        agent.printTransitions()
  }
}

object CCSCommand extends Command {
  val name = "ccs"
  val helpShort = "show CCS syntax"
  val helpDetailed = """
      |ccs; 
  |show all CCS syntax
  |ccs act; 
  |show syntax of CCS actions
  |ccs agent; 
  |show syntax of CCS agents
  |ccs relabel; 
  |show syntax of CCS relabelling functions

  |The formatting's not great, sorry: you'll find it more convenient to 
  |consult the Web page or the user manual.""".stripMargin
  
  private val ccsSyntax =
    "ACT   a  tau  internal action \n" +
    "         n  name: an identifier beginning with a lower case letter \n" +
    "         'n  coname. This is an ASCIIfication of normal CCS's overbarred n. \n\n" +
    "AGENT A  0  deadlock (nil)" +
    "         a.A  action prefix \n" +
    "         A + A  (weak) choice \n" +
    "         A | A  parallel composition \n" +
    "         A \\ a  restriction of a single action \n" +
    "         A \\ S  restriction of a set \n" +
    "         A[R]  relabelling \n" +
    "         (A)  you can use brackets just as you'd expect \n" +
    "         X  agent variables begin with upper case \n"  +
    "\n" +
    " The order of precedence is as usual: Strong Summation binds the weakest\n" +
    " then Parallel Composition, Prefixing, and\n" +
    " finally Restriction and Relabelling. These precedence rules can be\n" +
    " overcome by using parentheses.\n"


  def apply(str: String) = {
    println(ccsSyntax)
  }
}


object CCSComponent extends Module {
  def name = "CCS Component"
      def description = "Support for the CCS language in the Edinburgh Concurrency Workbench"
      val commands = List(AgentCommand, PrintCommand, TransitionsCommand, RelabelCommand,
                          ClearCommand, CCSCommand)
      def getCommands = commands

      val parser = new CCSParser()


  private var _environment = new Environment()
  
  def environment = _environment
  
  // Scratch the old variables assigned.
  def clearEnv() = _environment = new Environment()

  def printAgent(sym: Symbol, ag: CCSAgent): Unit = {
    println("agent " + sym.name + " = " + ag.agentString)
  }

  def printRelabel(sym: Symbol, relabel: LitRelabel): Unit = {
    println("relabel " + sym.name + " = " + relabel.relabellingString)
  }


}